Step of Proof: l_before_transitivity
11,40
postcript
pdf
Inference at
*
1
1
1
I
of proof for Lemma
l
before
transitivity
:
1.
T
: Type
2.
l
:
T
List
3.
x
:
T
4.
y
:
T
5.
z
:
T
6. no_repeats(
T
;
l
)
7. [
x
;
y
]
l
8. [
y
;
z
]
l
[
z
]
[
z
]
latex
by Easy
latex
.
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
sublist
weakening
origin
l
l
[z] [z]
by Easy
. l
l
[z] [z]
by Easy
.
Q
x:A. B(x)
T